/**
 *
 * NP and NP-Complete.
 *
 * <p><strong>Circuit SAT</strong>
 *
 * <p>Circuit SAT is NP problem because an input assignment can be verified in polynomial time.
 *
 * <p>Cook's theorem: Circuit SAT is an NP Complete. Any problem $L$ in NP can be computed using a boolean combination circuit (i.e. computer). The circuit has polynomial number of elements and can be constructed in polynomial time. So Circuit SAT can be reduced to $L$.
 *
 *
 * <p><strong>SAT</strong>
 *
 * <p>Given: $n$ variables $x_i$ and a bolean formula which is a conjunction (AND) of all the clauses (e.g. clause is an expression where literals ($x_i$ or $x↖{−}_i$) OR together).
 *
 * <p>Goal: determine whether such a formula is satisfiable.
 *
 * <p>Reduce Circuit SAT to SAT: Let each gate output be a variable.
 *
 * <p><strong>NOT gate</strong>
 * <pre>{@literal
 *      ┌───┐
 *   x ─┤ 1 │○── k    
 *      └───┘          }</pre>
 * $k ⇔ ¬x $ can be expressed as $(x ⋁ k) ⋀ (¬x ⋁ ¬k)$
 *
 * <p><strong>AND gate</strong>
 * <pre>{@literal
 *   x ┐┌───┐
 *   y ┼┤ & ├─── k
 *   z ┘└───┘          }</pre>
 * $k ⇔ x ⋀ y ⋀ z $ can be expressed as $(x ⋁ ¬k) ⋀ (y ⋁ ¬k) ⋀ (z ⋁ ¬k) ⋀ (¬x ⋁ ¬y ⋁ ¬z ⋁ k)$
 *
 * <p><strong>OR gate</strong>
 * <pre>{@literal
 *   x ┐┌───┐
 *   y ┼┤≥1 ├─── k
 *   z ┘└───┘          }</pre>
 * $k ⇔ x ⋁ y ⋁ z $ can be expressed as $(¬x ⋁ k) ⋀ (¬y ⋁ k) ⋀ (¬z ⋁ k) ⋀ (x ⋁ y ⋁ z ⋁ ¬k)$
 *
 * <p>To convert a circuit to a SAT formula: at each gate, create an equivalence expression between the output and input variables, then AND all of these expressions. For example:
 * <pre>{@literal
 *   a ─┐┌───┐
 *      ├┤ & ├── u ────┐
 *   b ─┘└───┘         │┌───┐
 *                     ├┤≥1 ├─── k
 *      ┌───┐          │└───┘   
 *   c ─┤ 1 │─○─ w ────┘ 
 *      └───┘          
 * }</pre>
 * Three expressions are created for corresponding gates: $k ⇔ (u ⋁ w)$, $u ⇔ (a ⋀ b)$, $w ⇔ ¬c$. This circuit can be formulated as:
 * $$k ⋀ (k ⇔ (u ⋁ w)) ⋀ (u ⇔ (a ⋀ b)) ⋀ (w ⇔ ¬c)$$
 * The above formula can be expressed as SAT formula:
 * $$k ⋀ (¬u ⋁ k) ⋀ (¬w ⋁ k) ⋀ (u ⋁ w ⋁ ¬k) ⋀ (a ⋁ ¬u) ⋀ (b ⋁ ¬u) ⋀ (¬a ⋁ ¬b ⋁ u) ⋀ (w ⋁ c) ⋀ (¬w ⋁ ¬c)$$
 *
 *
 * <p><strong>3SAT</strong>
 * 
 * <p>Reduce SAT to 3SAT: Convert any clause into equivalent collection of 3-literal clauses by adding some dummy variables.
 *
 * <p>One-literal clause: $(a) ⇔ (a ⋁ x ⋁ y) ⋀ (a ⋁ x ⋁ ¬y) ⋀ (a ⋁ ¬x ⋁ y) ⋀ (a ⋁ ¬x ⋁ ¬y)$
 * 
 * <p>Two-literal clause: $(a ⋁ b) ⇔ (a ⋁ b ⋁ x) ⋀ (a ⋁ b ⋁ ¬x)$
 *
 * <p>Three-literal clause: no conversion
 * 
 * <p>Four-literal clause: $(a ⋁ b ⋁ c ⋁ d) ⇔ (a ⋁ b ⋁ x) ⋀ (¬x ⋁ c ⋁ d)$
 *
 *
 * <p>N-literal clause: $(a ⋁ b ⋁ c ⋁ d ⋁ e ⋁ f) ⇔ (a ⋁ b ⋁ x) ⋀ (¬x ⋁ c ⋁ y) ⋀ (¬y ⋁ d ⋁ z) ⋀ (¬z ⋁ e ⋁ f)$
 *
 * <p>Reduce 3SAT to 3D Matching:
 *
 * <p>Example: 4 variables $x_1, x_2, x_3, x_4$ and 5 clauses
 * <ul>
 *  <li>$x_1 ⋁ x_2 ⋁ ¬x_3$
 *  <li>$¬x_1 ⋁ ¬x_2 ⋁ x_4$
 *  <li>$x_2 ⋁ ¬x_3 ⋁ ¬x_4$
 *  <li>$¬x_1 ⋁ x_3 ⋁ x_4$
 *  <li>$x_1 ⋁ x_3 ⋁ x_4$
 * </ul>
 *
 * <p><img src="../../../../../images/3SAT_3D_Match.svg" alt="3SAT to 3D Matching">
 *
 * <p>Constructions: Assuming n variables and m clauses.
 * <ul>
 *  <li>Construct $n$ gargets, each garget for one variable. In each garget, there are $m$ red core vertices, $m$ blue core vertices, $m$ positive (dark green) tip gargets and $m$ negative (light green) tip gargets. There are $2m$ triangles (each triangle has one red, one blue and one green (either dark or light) vertices).
 *  <li>Create $m$ clauses, each clause has one red vertex and one green vertex. Each clause has 3 triangles: each triangle contains the 2 red and green vertices, and one green tip vertex. But which green vertex is selected? The selected green vertex must not be selected before for another clause. Which vertex is selected depends on the clause. Take clause one as the example: $x_1 ⋁ x_2 ⋁ ¬x_3$: one triangle will select dark green (positive) tip vertex from garget 1 (corresponding to element $x_1$), one triangle will select dark green (positive) tip vertex from garget 2 (corresponding to element $x_2$), and one triangle will select light green (negative) tip vertex from garget 3 (corresponding to element $¬x_3$).
 *  <li>Create $m(n-1)$ dummy clauses. Each clause will create triangles for each green tip vertex (i.e. $2m$ triangles per clause).
 *  <li>So far, there are $2mn$ red vertices (set $R$), $2mn$ blue vertices (set $B$), $2mn$ green vertices (set $G$), and many triangles (set of triples $T ⊆ R×B×G$).
 * </ul>
 *
 * <p>Claim: $T$ has a match ⇔ 3SAT is satisfiable.
 *
 * <p><strong>Subset Sum Problem.</strong>
 * <p>Given: set $X$, size $s(x)$ for each item $x ∈ X$ and an integer $B$.
 * <p>Goal: determine if there is a subset $X'$ in $X$ such that: $∑↙{x ∈ X'}s(x) = B $.
 *
 * <p>Reduce 3SAT to Subset Sum: Take the above example of 4 variables and 5 clauses.
 *
 * <p>The idea is to represent variables and clauses with set numbers and find a subset sum that makes the 3SAT satisfiable. Look at a set of (n+m) digit numbers. The first n digit represent the variables and the last m digit represent the clauses. Let $T_i$ represent the literal $x_i$ and $F_i$ represent the literal $¬x_i$. Both $T_i$ and $F_i$ has 1 in the position i and 0 elsewhere in the first n digits. Within the last m digits, if clause $c_j$ has literal $x_i$ then $T_i$ has 1 in the position $j$, if the clause has literal $¬x_i$ then $F_i$ has 1 in the position $j$.
 *
 * <p>We need to target the subset sum such that either $T_i$ or $F_i$ (but not both) is selected for each variable $i$. So if the subset sum target contains all 1 for the first n digit, that will satisfy this requirement. 
 *
 * <p>Now look at the last m digits which represent the clauses. We want to target the subset sum that satisfies all the clauses. A clause $j$ is satisfied the sum at digit $j$ of the last m digits is greater than 0 (either 1, 2 or 3). Because we need a fixed number for the sum, we add a few dummy numbers. For each clause $j$, we add 2 dummy number $d_j$ and $D_j$ where $d_j$ has 1 at the position $j$ while $D_j$ has 2 at the position $j$. With this trick, we can now target the subset sum to be 4 in all the last m digits.
 *
 * <p>So far we have not mentioned the base of these numbers. We want the base large enough to make sure there is no carry when adding numbers in a particular subset. The max possible sum for a particular digit is 6. So we can select base 10 (which is sufficiently large and easy to compute).
 *
 * <pre>
 *                        x     clauses       decimal
 *                     ─────── ─────────      number 
 *                     1 2 3 4 1 2 3 4 5      set
 *                     ─────── ─────────      ─────────
 *               T1    1 0 0 0 1 0 0 0 1      100010001
 *               F1    1 0 0 0 0 1 0 1 0      100001010
 *               T2    0 1 0 0 1 0 1 0 0       10010100
 *               F2    0 1 0 0 0 1 0 0 0       10001000
 *               T3    0 0 1 0 0 0 0 1 1        1000011
 *               F3    0 0 1 0 1 0 1 0 0        1010100
 *               T4    0 0 0 1 0 1 0 1 1         101011
 *               F4    0 0 0 1 0 0 1 0 0         100100
 *               D1    0 0 0 0 1 0 0 0 0          10000
 *               E1    0 0 0 0 2 0 0 0 0          20000
 *               d2    0 0 0 0 0 1 0 0 0           1000
 *               D2    0 0 0 0 0 2 0 0 0           2000
 *               d3    0 0 0 0 0 0 1 0 0            100
 *               D3    0 0 0 0 0 0 2 0 0            200
 *               d4    0 0 0 0 0 0 0 1 0             10
 *               D4    0 0 0 0 0 0 0 2 0             20
 *               d5    0 0 0 0 0 0 0 0 1              1
 *               D5    0 0 0 0 0 0 0 0 2              2
 *                     ─────────────────      ─────────
 *           Target    1 1 1 1 4 4 4 4 4      111144444 (max: 222266666)
 *
 * </pre>
 * 
 *
 * <p><strong>Partition Problem.</strong>
 *
 * <p>Given: set $X$ and size $s(x)$ for each item $x ∈ X$.
 *
 * <p>Goal: determine if there is a subset $X'$ in $X$ such that $∑↙{x ∈ X'}s(x) = ∑↙{x ∈ X\\X'}s(x) $.
 *
 *
 * <p><strong>Vertex Cover.</strong>
 *
 * <p>Reduce 3SAT to Vertex Cover:
 *
 * <p><img src="../../../../../images/3SAT_Vertex_Cover.svg" alt="3SAT to Vertex Cover">
 *
 * <p>Construct a graph with $3m+2n$ vertices. That basically contains $m$ triangles (to represent all the clauses) and $n$ pairs (to represent variables). Shaded nodes represent negative literals.
 *
 * <p>Claim: 3SAT is satisified iff there is a vertex cover of size $2m+n$.
 *
 * <p>Proof: Suppose there is a vertex cover of size $2m+n$. The vertex cover must have at least two vertices for each triable and at least one vertex for each pair. So the vertex cover must have at least $2m+n$ vertices. As we found a vertex cover of size $2m+n$, this cover must contain exactly two vertices in each triangle and one vertex in each pair. It can easily show that the free vertices are the solution to make 3SAT satisfied.
 *
 * <p>On the other hand, if the 3SAT is satisfied, it can easily show that there is a vertex cover of size $3m+n$.
 *
 *
 * <p><strong>Independent Set.</strong>
 * <p><img src="../../../../../images/3SAT_Independent_Set.svg" alt="3SAT to Independent Set">
 *
 * <p>Claim: 3SAT is satisified iff there is an independent set of size $m$.
 *
 * <p><strong>Hamilton Cycle.</strong>
 *
 * <p>Reduce 3SAT to Hamilton Cycle:
 *
 * <p><img src="../../../../../images/3SAT_Hamilton_Cycle.svg" alt="3SAT to Hamilton Cycle">
 *
 *
 *
 *
 * 
 * @author Trung Phan
 *
 */
package net.tp.algo.np;
